\begin{tabbing}
$\forall$\=$i$,$x$:Id, $T$:Type, ${\it ds}$:fpf(Id; $x$.Type), $f$:(\=(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+\+\+
\\[0ex](\=${\it ds}$; $x$\+
\\[0ex])) + (decl{-}state(${\it ds}$)
\-\-\\[0ex]$\rightarrow$$T$$\rightarrow$rationals$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$))),
\-\-\\[0ex]$k$:Knd, $A$:es\_realizer\{i:l\}.
\-\\[0ex]R{-}Feasible\=\{i:l\}\+
\\[0ex]($A$)
\-\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$R{-}occurs($A$; $i$; $x$)))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; R{-}ds($A$; $i$))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Knd; $k$.Type; Kind{-}deq; fpf{-}single($k$; $T$); R{-}da($A$; $i$))
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ subtype\_rel(fpf{-}cap(R{-}da($A$; source(lnk($k$))); Kind{-}deq; $k$; void); $T$))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$write{-}restricted($A$; $i$; $k$)))
\\[0ex]$\Rightarrow$ ($\forall$$y$:Id. ($\uparrow$fpf{-}dom(id{-}deq; $y$; ${\it ds}$)) $\Rightarrow$ ($\neg$($\uparrow$read{-}restricted($A$; $i$; $y$))))
\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](Reffect($i$; ${\it ds}$; $k$; $T$; $x$; $f$); $A$)
\-
\end{tabbing}